Nuprl Lemma : fpf-ap_functionality
0,22
postcript
pdf
eq1
,
eq2
,
f
,
x
:Top.
f
(
x
) ~
f
(
x
)
latex
Definitions
f
(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
origin
eq1, eq2, f, x:Top. f(x) ~ f(x) eq1, eq2, f, x:Top. f(x) ~ f(x) x:A. B(x)
T